$\forall$${\it es}$:ES, $L$:E List. loc{-}ordered(${\it es}$;$L$) $\in$ Prop